Nuprl Lemma : ma-join-list-is-empty
0,22
postcript
pdf
L
:MsgA List. ma-is-empty(
(
L
)) ~ reduce(
M
,
x
. ma-is-empty(
M
)
x
;true
;
L
)
latex
Definitions
x
:
A
.
B
(
x
)
,
(
L
)
,
reduce(
f
;
k
;
as
)
,
Y
,
t
T
,
ma-is-empty(
M
)
,
,
true
,
p
q
,
fpf-is-empty(
f
)
,
1of(
t
)
,
mk-ma
,
,
2of(
t
)
,
i
=
j
,
||
as
||
,
if
b
t
else
f
fi
,
P
Q
,
SQType(
T
)
,
{
T
}
Lemmas
msga
wf
,
msg-form
wf
,
msg-form-join-list
,
bool
sq
origin
L:MsgA List. ma-is-empty(
(L)) ~ reduce(
M,x. ma-is-empty(M) 
x;true;L) L:MsgA List. ma-is-empty((L)) ~ reduce(M,x. ma-is-empty(M) x;true;L) x:A. B(x)(L)
T qj
t else f fi
Q